package kodkod.analysis.ast;

import java.text.DecimalFormat;
import java.text.NumberFormat;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.TreeSet;

import kodkod.analysis.Problem;
import kodkod.ast.*;
import kodkod.ast.operator.ExprCastOperator;
import kodkod.engine.fol2sat.Skolemizer;
import kodkod.engine.fol2sat.Translation;

public class wNode implements Comparable<wNode> {
	Graph graph;
	public Node node;
		
	/* provide possibility to enable recursive names */
	private boolean recursiveMode = false;
	
	TreeSet<wEdge> incomingEdges = new TreeSet<wEdge>();
	TreeSet<wEdge> outgoingEdges = new TreeSet<wEdge>();
	
	public String fillcolor = "white";
	
	public double weight = 0.0;
	public boolean primary = false;
	public int primaryIndex = -1;
	
	public boolean negated = false;	
	public wCompoundNode compound = null;	
	public static Translation translation = null;
	
	
				
	protected wNode(Graph graph, Node node) {
		this.graph = graph;
		this.node = node;
	}
	
	public void setRecursiveMode(boolean rm) {
		this.recursiveMode = rm;
	}
	
	protected void addIncomingEdge(wEdge edge) {
		incomingEdges.add(edge);
	}
	
	protected void addOutgoingEdge(wEdge edge) {
		outgoingEdges.add(edge);
	}
	
	public TreeSet<wEdge> getIncomingEdges() {
		return incomingEdges;
	}
	
	public TreeSet<wEdge> getOutgoingEdges() {
		return outgoingEdges;
	}
	
	public Integer getId() {
		Integer id = graph.nodeIds.get(node);
		if (id == null) {
			id = graph.idCounter++;
			graph.nodeIds.put(node, id);
		}
		if (graph.idCounter < 0) {
			graph.idCounter = 0;
		}		
		return id;
	}
	
	public String getIdString() {
		if (this instanceof wCompoundNode) {
			return "N" + getId() + ":" + "N" + getId();
		} else if (compound != null) {
			return "N" + compound.getId() + ":" + "N" + getId();			
		} else {
			return "N" + getId();
		}
	}

	@Override	
	public int compareTo(wNode w) {
		return getId().compareTo(w.getId());
	}
	
	@Override
	public boolean equals(Object o) {
		if (o == null || !(o instanceof wNode)) {
			return false;
		}
		return ((wNode)o).node == node;
	}
	
	@Override	
	public int hashCode() {
		return getId();
	}
	
	public String getLabel() {
		String name = getName(node);
		if (node instanceof LeafExpression && primaryIndex != -1) {
			name = primaryIndex + ": " + name + "\\n";
			NumberFormat format = new DecimalFormat("#0.000");
			name += format.format(weight) + "\\n";
		}
		return name;
	}
	
	@Override
	public String toString() {
		StringBuffer nodeString = new StringBuffer();
		nodeString.append("N"+getId()+" [");
		nodeString.append("label=\""+getLabel()+"\"");
		if (this instanceof wCompoundNode) {
			nodeString.append(", shape=record");
		} else if (node instanceof Formula) {
			nodeString.append(", shape=triangle");
		} else if (node instanceof Expression) {
			if (node instanceof LeafExpression) {
				if (node instanceof Variable) {
					nodeString.append(", shape=ellipse");
				} else {
					nodeString.append(", shape=box");
				}
			} else {
				nodeString.append(", shape=diamond");
			}
		} else if (node instanceof Decls) {
			nodeString.append(", shape=Mcircle");
		} else if (node instanceof IntExpression) {
			nodeString.append(", shape=pentagon");
		}
		
		if (this.primary) {
			nodeString.append(", fontcolor=red");
			nodeString.append(", group=\"primary\"");
		}
		
		nodeString.append(", style=filled, fillcolor=\""+fillcolor+"\"]");
		return nodeString.toString();
	}
	
	protected String getName(Node node) {
		if (node instanceof Decls) {
			return "Decl";
		}
		if (node instanceof Expression) {
			if (node instanceof UnaryExpression) {
				UnaryExpression exp = (UnaryExpression)node;
				String name = exp.op().toString();
				if (recursiveMode) {
					return name + "(" + getName(exp.expression()) + ")";
				} else {
					return name;
				}
			}
			if (node instanceof BinaryExpression) {
				BinaryExpression exp = (BinaryExpression)node;
				String name = exp.op().toString();
				if (recursiveMode) {
					return "(" + getName(exp.left()) + name + getName(exp.right()) + ")";
				} else {
					return name;
				}
			}
			if (node instanceof NaryExpression) {
				NaryExpression exp = (NaryExpression)node;
				String name = exp.op().toString();
				if (recursiveMode) {
					StringBuilder builder = new StringBuilder();
					boolean start = true;
					for (Expression child : exp) {
						if (!start) builder.append(name);
						builder.append(getName(child));
						start = false;
					}					
					return "(" + builder.toString() + ")";
				} else {
					return name;
				}
			}
			if (node instanceof Comprehension) {
				return "{Set}";
			}
			if (node instanceof IfExpression) {
				return "If";
			}
			if (node instanceof ProjectExpression) {
				return "project";
			}
			if (node instanceof IntToExprCast) {
				return ((IntToExprCast)node).op().name();
			}
			if (node instanceof LeafExpression) {
				if (node instanceof ConstantExpression) {
					return ((ConstantExpression)node).name();
				}
				if (node instanceof Relation) {
					return ((Relation)node).name();
				}
				if (node instanceof Variable) {
					return "$"+((Variable)node).name();
				}
				return "UnspecifiedLeafExpression";
			}
			return "UnspecifiedExpression";
		}
		if (node instanceof Formula) {
			if (node instanceof IntComparisonFormula) {
				return ((IntComparisonFormula)node).op().toString();
			}
			if (node instanceof QuantifiedFormula) {
				return ((QuantifiedFormula)node).quantifier().toString();
			}
			if (node instanceof NaryFormula) {
				return ((NaryFormula)node).op().toString();
			}
			if (node instanceof BinaryFormula) {
				return ((BinaryFormula)node).op().toString();
			}
			if (node instanceof NotFormula) {
				return "NOT";
			}
			if (node instanceof ComparisonFormula) {
				return ((ComparisonFormula)node).op().toString();
			}
			if (node instanceof MultiplicityFormula) {
				return ((MultiplicityFormula)node).multiplicity().toString();
			}
			if (node instanceof RelationPredicate) {
				switch (((RelationPredicate)node).name()) {
				case FUNCTION :
					return "RP.Func";
				case TOTAL_ORDERING :
					return "RP.TotOrd";
				case ACYCLIC :
					return "RP.Acyc";
				default :
					return "UnspecifiedRelationPredicate";
				}
			}
			if (node instanceof ConstantFormula) {
				return ((ConstantFormula)node).toString();
			}
			return "UnspecifiedFormula";
		}
		if (node instanceof IntExpression) {
			if (node instanceof ExprToIntCast) {
				ExprToIntCast cast = (ExprToIntCast)node;
				if (cast.op() == ExprCastOperator.CARDINALITY) {
					return "#";
				} else if (cast.op() == ExprCastOperator.SUM) {
					return "sum";
				} else {
					return "toInt";
				}
			}
			if (node instanceof NaryIntExpression) {
				return ((NaryIntExpression)node).op().toString();
			}
			if (node instanceof BinaryIntExpression) {
				return ((BinaryIntExpression)node).op().toString();
			}
			if (node instanceof UnaryIntExpression) {
				return ((UnaryIntExpression)node).op().toString();
			}
			if (node instanceof SumExpression) {
				return "SUM";
			}
			if (node instanceof IfIntExpression) {
				return "If";
			}
			if (node instanceof IntConstant) {
				return ((IntConstant)node).toString();
			}
			return "UnspecifiedIntExpression";
		}
		
		return "UnspecifiedNode";
	}
}